Skip to content

Simplify kompilation for proof tests#2430

Merged
rv-jenkins merged 5 commits intomasterfrom
kompile-cache
May 20, 2024
Merged

Simplify kompilation for proof tests#2430
rv-jenkins merged 5 commits intomasterfrom
kompile-cache

Conversation

@tothtamas28
Copy link
Contributor

Fixes #2419

  • Remove the kompiled_target_cache fixture
  • Do not require directory passed as --kompiled-targets-dir to exist
  • Simplify target directory layout
  • Use a soft file lock
  • Renamings

@tothtamas28 tothtamas28 self-assigned this May 16, 2024
@tothtamas28 tothtamas28 changed the title Simplify komppilation for proof tests Simplify kompilation for proof tests May 16, 2024
@tothtamas28 tothtamas28 requested a review from geo2a May 17, 2024 14:59
@tothtamas28 tothtamas28 marked this pull request as ready for review May 17, 2024 14:59
parser.addoption(
'--kompiled-targets-dir',
type=dir_path,
'--kompiled-target-dir',
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

May I ask you to not change this name, as our performance script uses the old one?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done.

ids=[str(spec_file.relative_to(SPEC_DIR)) for spec_file in ALL_TESTS],
)
def test_kompile_targets(spec_file: Path, kompiled_target_for: Callable[[Path], Path], request: FixtureRequest) -> None:
def test_kompile(
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same request as above, would it be possible to not change this name too?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done.

Copy link
Contributor

@geo2a geo2a left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please do not change the names of the command line arguments and the test that prekompiles the defintions.

Copy link
Contributor

@geo2a geo2a left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks @tothtamas28 !

@rv-jenkins rv-jenkins merged commit b076ddc into master May 20, 2024
@rv-jenkins rv-jenkins deleted the kompile-cache branch May 20, 2024 17:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Refactor kompilation cache in the intergration tests

4 participants

Comments